T:Type, L:(T List), x:T. (x  rev(L))  (x  L) 

latex

Definitions

{x:A| B(x)} , ||as||, Y, x.A(x), rec-case(a) of [] => s | x::y => z.t(x;y;z), n+m, l[i], hd(l), nth_tl(n;as), if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), i z j, b, i <z j, if a<b then c else d, n - m, tl(l), as @ bs, [car / cdr], x. t(x), , , Unit, |r|, |g|, |p|, x,y:A//B(x;y), {i..j}, Atom, , (xL.P(x)), xL. P(x), x f y, f(a), A c B, a < b, a <p b, a  b, a ~ b, b | a, b, A  B, A, False, Dec(P), , {T}, a < b, x:A. B(x), P  Q, left + right, rev(as), P & Q, x:A  B(x), P  Q, P  Q, s = t, t  T, [], Type, x:A. B(x), P  Q, (x  l), x:AB(x), type List

Lemmas

iff wf, l member wf, cons member, rev implies wf, or functionality wrt iff, iff functionality wrt iff, all functionality wrt iff, member append, nil member